k:Knd, mTyp, vTyp:Type, ds:x:Id fp Type, l:IdLnk, tg:Id, f:((:State(ds)  vTyp)(mTyp + Top)),
es:ES.
k(v:vTyp) sends on l [tg:mTyp, f <state, v>]?[]   

latex

Definitions

s ~ t, loc(e), source(l), k(v:B) sends on l [tg:T, f <state, v>]?[], do-apply(f;x), if b then t else f fi , kind(e), rcv(l,tg), case b of inl(x) => s(x) | inr(y) => t(y), True, tt, ff, can-apply(f;x), val(e), suptype(S; T), S  T, (state when e), SQType(T), State(ds), x. t(x), x.A(x), IdDeq, f(x)?z, vartype(i;x), valtype(e), state@i, <a, b>, x:A.B(x), Void, , x:A. B(x), Top, constant_function(f;A;B), , r  s, e < e', val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), , , type List, Msg(M), kindcase(k; a.f(a); l,t.g(l;t) ), EState(T), f(a), EOrderAxioms(E; pred?; info), Unit, EqDecider(T), let x,y = A in B(x;y), sender(e), A, False, s = t, E, t.1, ES, x:AB(x), Id, Atom$n, IdLnk, a:A fp B(a), Type, Knd, left + right, b, isrcv(e), x:A. B(x), P  Q, {T}, A c B, P & Q, x:A  B(x), t  T

Lemmas

es-kind-rcv, es-sender wf, not wf, false wf, subtype rel sum, es-vartype wf, id-deq wf, fpf-cap wf, es-state-subtype, subtype rel product, Id sq, es-state-when wf, es-state wf, subtype rel function, can-apply wf, assert wf, bfalse wf, btrue wf, es-val wf, true wf, rcv wf, es-kind wf, do-apply wf, top wf, es-valtype wf, Knd wf, lsrc wf, es-loc wf, es-E wf, Id wf, fpf wf, IdLnk wf, decl-state wf, event system wf